T:Type, l1, l2:(T List).
l1  l2  ((||l1||  ||l2||) c (i:. (i < ||l1||)  (l1[i] = l2[i]  T))) 

latex

Definitions	t  T, x:A. B(x), , P  Q, P & Q, Y, P  Q, ||as||, A c B, P  Q, False, A, A  B, {T}, SQType(T), , True, T, x:A. B(x), l1  l2, as @ bs, P  Q, Dec(P), ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), l[i]
Lemmas	length wf2, select wf, le wf, nil iseg, iseg wf, nat wf, non neg length, length wf1, length append, append wf, cons iseg, decidable int equal, select cons hd, select cons tl, squash wf